#include "configuration.h"
#include "predicates.h"
#include "tree.h"

const std::string space = " ";

Operator const operators[] = { //
    { "#", +0 }, // Rules separator
    { inferenceOperator, 0 }, // :-
    { "!", +0 }, // Cut
    { "=>", 0 }, // If-then clause in select statement. Not >=
    { "| ", 0 }, // General divisor
    { ";", +0 }, // Or
    { ",", +0 }, // And
    { "<=", 0 }, // Comparisons
    { "<", +0 }, // "
    { ">=", 0 }, // "
    { ">", +0 }, // "
    { "=", +0 }, // Equality
    { "+", +0 }, // Arithmetics
    { "- ", 1 }, // "
    { "*", +0 }, // "
    { "/ ", 1 }, // "
    { "^", +0 }, // Power
    { " ", +0 }, // Tuple separator
    { ":", +0 }, // Pairs
    { "|", +0 }, // Smaller pairs
    };

const int nOperators = sizeof(operators) / sizeof(operators[0]);

int tupleOperator () {
  for(int n = 0; n < nOperators; n++)
    if(strcmp (operators[n].name, " ") == 0)
      return n;
  return nOperators; // Should not be reached
}

int Tree::findOperatorIndex () {
  for(int n = 0; n < nOperators; n++)
    if(strncmp (ops, operators[n].name, 2) == 0)
      return n;
  return nOperators;
}

std::string Tree::padOperator () {
  if(strcmp (ops, ":") == 0 || // Make these separators tighter
      strcmp (ops, "|") == 0)
    return (std::string) ops;
  else if(strcmp (ops, ";") == 0 || strcmp (ops, ",") == 0)
    return ((std::string) ops) + space; // + "\n  "; // Pretty print
  else if(ops[1] == ' ')
    return space + opString ();
  else if(strcmp (ops, "#") == 0) // Each rule on a new line
    return " " + (std::string) ops + "\n";
  else
    return space + opString () + space;
}

std::string Tree::dump (int precedence) {
  int index = findOperatorIndex ();

  // See if parentheses are needed
  int rightAssociated = operators[index].rightAssociation;

  if(index < precedence || index == nOperators)
    return '(' + left .node->dump (index + !rightAssociated) + padOperator ()
        + right.node->dump (index + rightAssociated) + ')';
  else
    return left .node->dump (index + !rightAssociated) + padOperator ()
        + right.node->dump (index + rightAssociated);
}

std::string Tree::display (int precedence) {
  int index = findOperatorIndex ();
  int rightAssociated = operators[index].rightAssociation;

  if(index < precedence || index == nOperators)
    return '(' + left .node->display (index + !rightAssociated)
        + padOperator () + right.node->display (index + rightAssociated) + ')';
  else
    return left .node->display (index + !rightAssociated) + padOperator ()
        + right.node->display (index + rightAssociated);
}

pNode Tree::replicate () {
  if(fixed)
    return this;

  pNode replicatedLeft (left .node->replicate ());
  pNode replicatedRight (right.node->replicate ());
  Tree *ret = // No substitution
      (replicatedLeft == left && replicatedRight == right) ? this : new Tree (
          ops, replicatedLeft, replicatedRight);

  ret->fixed = true;
  return ret;
}

std::string Tree::opString () {
  if(ops[1] == 0)
    return std::string (ops);
  else
    return std::string (ops, 2);
}

class isTree : public OnceProver {
predicateName("is.tree")

  bool proveOnce () {
    return typeid(*tuple->nodes[1].final ()) == typeid(Tree);
  }

  Tuple *tuple;
  void set (Tuple &t, System&) {
    tuple = &t;
  }
};

ProverFactoryRegistrar<isTree, Tuple::ID, 2> isTreeRegistrar;
